A, C:Type, B:(AType), D:(CType), rinv:(C(A+Unit)), r:(AC), f:c:C fp D(c).
inv-rel(A;C;r;rinv)  (a:A. D(r(a)) = B(a))  fpf-inv-rename(r;rinv;f)  a:A fp B(a) 

latex

Definitions	P  Q, Prop, inv-rel(A;B;f;finv), x. t(x), Unit, fpf-inv-rename(r;rinv;f), a:A fp B(a), (x  l), x(s), x:A. B(x), t  T, mapfilter(f;P;L), outl(x), , SqStable(P), T, True, b, isl(x), f o g, P  Q, x:A. B(x), P & Q, A & B, False
Lemmas	false wf, true wf, member map filter, isl wf, assert wf, decidable assert, sq stable from decidable, outl wf, mapfilter wf, l member wf, unit wf, fpf wf, inv-rel wf